Nuprl Lemma : concat-cons
11,40
postcript
pdf
l
:(top List),
ll
:(top List List). sqequal(concat(cons(
l
;
ll
)); append(
l
; concat(
ll
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
concat(
ll
)
,
reduce(
f
;
k
;
as
)
,
Y
,
t
T
Lemmas
top
wf
origin
l:(top List), ll:(top List List). sqequal(concat(cons(l; ll)); append(l; concat(ll))) l:(top List), ll:(top List List). sqequal(concat(cons(l; ll)); append(l; concat(ll))) x:A. B(x)
T